(0) Obligation:

Clauses:

p(X, Y, Z) :- ','(=(X, Y), ','(=(Z, 1), !)).
p(X, Y, Z) :- ','(=(Z, 1), ','(=(Y, X), p(X, Y, Z))).
=(X, X).

Query: p(a,a,a)

(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

p(X, Y, Z) :- ','(user_defined_=(X, Y), ','(user_defined_=(Z, 1), !)).
p(X, Y, Z) :- ','(user_defined_=(Z, 1), ','(user_defined_=(Y, X), p(X, Y, Z))).
user_defined_=(X, X).

Query: p(a,a,a)

(3) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

(4) Obligation:

Clauses:

pA(T60).
pB(T15, T15, 1).
pB(T51, T51, 1) :- pA(T51).
pB(T92, T92, 1) :- pA(T92).

Query: pB(a,a,a)

(5) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
pB_in: (f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

pB_in_aaa(T15, T15, 1) → pB_out_aaa(T15, T15, 1)
pB_in_aaa(T51, T51, 1) → U1_aaa(T51, pA_in_a(T51))
pA_in_a(T60) → pA_out_a(T60)
U1_aaa(T51, pA_out_a(T51)) → pB_out_aaa(T51, T51, 1)
pB_in_aaa(T92, T92, 1) → U2_aaa(T92, pA_in_a(T92))
U2_aaa(T92, pA_out_a(T92)) → pB_out_aaa(T92, T92, 1)

The argument filtering Pi contains the following mapping:
pB_in_aaa(x1, x2, x3)  =  pB_in_aaa
pB_out_aaa(x1, x2, x3)  =  pB_out_aaa(x3)
U1_aaa(x1, x2)  =  U1_aaa(x2)
pA_in_a(x1)  =  pA_in_a
pA_out_a(x1)  =  pA_out_a
U2_aaa(x1, x2)  =  U2_aaa(x2)
1  =  1

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

pB_in_aaa(T15, T15, 1) → pB_out_aaa(T15, T15, 1)
pB_in_aaa(T51, T51, 1) → U1_aaa(T51, pA_in_a(T51))
pA_in_a(T60) → pA_out_a(T60)
U1_aaa(T51, pA_out_a(T51)) → pB_out_aaa(T51, T51, 1)
pB_in_aaa(T92, T92, 1) → U2_aaa(T92, pA_in_a(T92))
U2_aaa(T92, pA_out_a(T92)) → pB_out_aaa(T92, T92, 1)

The argument filtering Pi contains the following mapping:
pB_in_aaa(x1, x2, x3)  =  pB_in_aaa
pB_out_aaa(x1, x2, x3)  =  pB_out_aaa(x3)
U1_aaa(x1, x2)  =  U1_aaa(x2)
pA_in_a(x1)  =  pA_in_a
pA_out_a(x1)  =  pA_out_a
U2_aaa(x1, x2)  =  U2_aaa(x2)
1  =  1

(7) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

PB_IN_AAA(T51, T51, 1) → U1_AAA(T51, pA_in_a(T51))
PB_IN_AAA(T51, T51, 1) → PA_IN_A(T51)
PB_IN_AAA(T92, T92, 1) → U2_AAA(T92, pA_in_a(T92))

The TRS R consists of the following rules:

pB_in_aaa(T15, T15, 1) → pB_out_aaa(T15, T15, 1)
pB_in_aaa(T51, T51, 1) → U1_aaa(T51, pA_in_a(T51))
pA_in_a(T60) → pA_out_a(T60)
U1_aaa(T51, pA_out_a(T51)) → pB_out_aaa(T51, T51, 1)
pB_in_aaa(T92, T92, 1) → U2_aaa(T92, pA_in_a(T92))
U2_aaa(T92, pA_out_a(T92)) → pB_out_aaa(T92, T92, 1)

The argument filtering Pi contains the following mapping:
pB_in_aaa(x1, x2, x3)  =  pB_in_aaa
pB_out_aaa(x1, x2, x3)  =  pB_out_aaa(x3)
U1_aaa(x1, x2)  =  U1_aaa(x2)
pA_in_a(x1)  =  pA_in_a
pA_out_a(x1)  =  pA_out_a
U2_aaa(x1, x2)  =  U2_aaa(x2)
1  =  1
PB_IN_AAA(x1, x2, x3)  =  PB_IN_AAA
U1_AAA(x1, x2)  =  U1_AAA(x2)
PA_IN_A(x1)  =  PA_IN_A
U2_AAA(x1, x2)  =  U2_AAA(x2)

We have to consider all (P,R,Pi)-chains

(8) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PB_IN_AAA(T51, T51, 1) → U1_AAA(T51, pA_in_a(T51))
PB_IN_AAA(T51, T51, 1) → PA_IN_A(T51)
PB_IN_AAA(T92, T92, 1) → U2_AAA(T92, pA_in_a(T92))

The TRS R consists of the following rules:

pB_in_aaa(T15, T15, 1) → pB_out_aaa(T15, T15, 1)
pB_in_aaa(T51, T51, 1) → U1_aaa(T51, pA_in_a(T51))
pA_in_a(T60) → pA_out_a(T60)
U1_aaa(T51, pA_out_a(T51)) → pB_out_aaa(T51, T51, 1)
pB_in_aaa(T92, T92, 1) → U2_aaa(T92, pA_in_a(T92))
U2_aaa(T92, pA_out_a(T92)) → pB_out_aaa(T92, T92, 1)

The argument filtering Pi contains the following mapping:
pB_in_aaa(x1, x2, x3)  =  pB_in_aaa
pB_out_aaa(x1, x2, x3)  =  pB_out_aaa(x3)
U1_aaa(x1, x2)  =  U1_aaa(x2)
pA_in_a(x1)  =  pA_in_a
pA_out_a(x1)  =  pA_out_a
U2_aaa(x1, x2)  =  U2_aaa(x2)
1  =  1
PB_IN_AAA(x1, x2, x3)  =  PB_IN_AAA
U1_AAA(x1, x2)  =  U1_AAA(x2)
PA_IN_A(x1)  =  PA_IN_A
U2_AAA(x1, x2)  =  U2_AAA(x2)

We have to consider all (P,R,Pi)-chains

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 3 less nodes.

(10) TRUE